The present invention is related to verification of integrated circuit designs. More particularly, the present invention is directed to a method and system for verifying integrated circuit designs through partitioning.
Circuit designers and verification engineers use different methods to verify circuit designs. One common verification technique is simulation. Simulation dynamically verifies a design by monitoring behaviors of the design with respect to simulation test benches. Another verification technique is model checking. Model checking statically verifies properties of a design by analyzing the state space of the design and determining whether a property holds in all reachable states. The properties to verify may be global properties involving signals in widely separated parts of the design, or they may be more local properties that pertain only to single or small number of related modules in the design.
As used herein, the term “module” refers to any part of an integrated circuit design. A module may comprise, for example, one or more functional components or a part of each of one or more functional components. A module is generally parameterized and thus may be instantiated one or more times in an integrated circuit design to describe “instances” of that module. An integrated circuit design in this case is comprised of module instances.
There are two distinct classes of local properties: built-in and user-specified. The built-in properties are those that can be inferred from the structure of the design, for example, the absence of arithmetic overflow, range overflow, index overflow, bus contention, multi-driven bus, divide by zero, and combinational cycles. The user-specified properties are those that are explicitly provided by the user, for example, as synthesis pragmas or as assertions defined in assertion language.
Model checking has potential advantages over simulation. For example, no simulation test bench is required to run model checking. Moreover, model checking, unlike simulation, is exhaustive. On the other hand, model checking, due to computational limitations, generally cannot handle large designs. Hence, designs must often be partitioned into sufficiently small parts in order to model check a given property. Although presently capacity is not an issue for simulation of designs, it is foreseeable that in the future designs could be of a size that cannot be handled by a simulator as a whole.
Model checking is also sensitive to assumptions about the environment of the portion of the design being checked, and is prone to generating false negatives, i.e., reports of failures that cannot actually happen, if sufficient information about the environment is not included in the run. There may be an accuracy versus performance trade-off in different partitioning strategies. A partitioning strategy that generates the minimum number of computationally tractable non-overlapping partitions could be the most computationally efficient but could lead to a large number of false negatives. Consequently, there is a need for partitioning algorithms that provides a balance between accuracy and performance.
The present invention provides a method and system for verifying integrated circuit designs through partitioning. In an embodiment, a design is partitioned, then verification is applied to each partition. In one embodiment, the design is partitioned at the granularity of modules. In another embodiment, the design is partitioned at the granularity of instances. In a further embodiment, the design is partitioned to avoid redundant partitions. In an embodiment, model checking is applied to local properties of each partition. In another embodiment, simulation is used to verify each partition.
Further details of aspects, objects, and advantages of the invention are described below in the detailed description, drawings, and claims. Both the foregoing general description and the following detailed description are exemplary and explanatory, and are not intended to be limiting as to the scope of the invention.